Section: New Results

Incremental development of distributed algorithms

Participants : Dominique Méry, Manamiary Andriamiarina.

The development of distributed algorithms and, more generally, of distributed systems, is a complex, delicate, and challenging process. The approach based on refinement helps to gain formality by using a proof assistant, and proposes to apply a design methodology that starts from the most abstract model and leads, in an incremental way, to the most concrete model, for producing a distributed solution. Our works help to formalize pre-existing algorithms, develop new algorithms, as well as develop models for distributed systems.

Our research, carried out with Mohammed Mosbah and Mohammed Tounsi from the LABRI laboratory, was supported by the ANR project RIMEL until 2010 and we are maintaining a joint project B2VISIDIA with LABRI on these topics. More concretely, we aim at an integration of the correct-by-construction refinement-based approach into the local computation programming model. The team of LABRI develops an environment called VISIDIA that provides a toolset for developing distributed algorithms expressed as a set of rewriting rules of graph structures. The simulation of rewriting rules is based on synchronization algorithms and we have developed these algorithms by refinement.

Synchronization algorithms [14] are mandatory for simulating local computation models of distributed algorithms. Therefore, correctness of these algorithms becomes crucial, because it gives confidence that local computations are simulated as designed and do not behave harmfully. However, these algorithms are often very complex to prove correct since they integrate both distributed and probabilistic aspects. We derive proofs of synchronization algorithms upon which the correct-by-construction paradigm depends; the latter is supported by a progressive and incremental process controlled by the refinement techniques. We illustrate our approach by examples such as the Handshake and the LC1 algorithms. These algorithms are designed for an asynchronous distributed network of anonymous processes that communicate by message passing.

A second contribution is related to the integration of probabilistic arguments when reasoning about the design of distributed programms. We particularly focus [20] on probabilistic aspects of distributed algorithms related to termination, e.g. the choice between two delays in the case of communication protocols like IEEE 1394 (FireWire), or the choice between several colors for vertex coloring algorithms. We have in particular applied this approach to developing probabilistic distributed graph coloring algorithms (also called vertex coloring algorithms), based on an algorithm developed by Métivier et al. [32] , using the Event B and probabilistic Event B methods.

A third contribution takes into account the modification of links between nodes in a graph modelling a network. We present [15] an incremental formal development of the Dynamic Source Routing (DSR) protocol in Event-B. DSR is a reactive routing protocol, which finds a route for a destination on demand, whenever communication is needed. Route discovery is an important task of any routing algorithm and its formal specification is a challenging problem in itself. The specification is performed in a stepwise manner by introducing more advanced routing components between the abstract specification and topology. It is verified through a series of refinements. The specification includes safety properties as a set of invariants, and liveness properties that characterize when the system reaches stable states. We establish these properties by proof of invariants, event refinement and deadlock freedom. The consequence of this incremental approach helps us achieve a high degree of automatization. Our approach can be useful for formalizing and developing other kinds of reactive routing protocols such as AODV.